g:Mon, a, b:|g|. (a = b) = (b = a)   

latex

Up	groups 1
Definitions of Statement	Mon
Definitions	, P  Q, P & Q, t  T, P  Q, P  Q, x f y, x:A. B(x), Mon
Lemmas	mon wf, assert of mon eq, grp car wf, assert wf, iff functionality wrt iff, grp eq wf, iff imp equal bool